As expert system technology gains wider acceptance in digital system design, the need to build and maintain a large scale knowledge base will assume greater importance. However, how to build a correct and efficient rule base is even a hard part in the knowledge-based system development. In this paper, we develop FARHDL (Frame-And-Rule-based Hardware Description Language) to form a knowledge base. The FARHDL is simple but powerful to specify the hardware requirements and can be directly simulated by PROLOG. Through the knowledge base transformed from FARHDL, a formal method can be developed to design, implement, and validate the digital hardware systems. Furthermore, behavioral properties, anomaly properties, structural properties, and timing properties are applied to analyze the requirements specification. The purposes of those properties are used to detect explicit/implicit incorrect specification clauses and to capture some desired requirements, such as completeness and consistency. Finally, the analysis results can be a useful tool for finding obscure problems in tricky digital system designs and can also aid in the development of formal specifications.

Estimating the deadline of a real-time task is a necessary prerequisite to the applications that have strict timing constraints, such as real-time systems design. This paper shows how Monte-Carlo simulation can be used as a space-efficient way of analyzing Timed Petri nets to predict whether the system specified can satisfy its real-time deadlines. For the purpose, Extended Timed Petri Net (XTPN), an extension of conventional Timed Petri net, and its execution rule, using Monte-Carlo technique, are newly defined. A simple simulation scheme with less memory space is presented as a way of estimating the deadline of a real-time task modeled in XTPN. And the comparison between the analytical and simulation results is given. The problem addressed here is to find the probabilities of meeting given deadlines.

Petri nets are one of useful models for discrete event systems in which liveness problem as well as reachability problem is one of big issues. But, it has not been completely solved from the point of view of useful initial-marking-based liveness conditions in general Petri nets. In this paper, to guarantee local liveness (i. e. , liveness underMoD) for each minimal deadlock (MSDL),ND=(SD,TD,FD,MoD), with real deadlock-trap structure, it is shown that the minimum number of required live minimal structural traps (MSTRs),NT=(ST,TT,FT,MoT) s. t. SD ST, is conditionally (which means that the conditions of Lemma 4-9 are fulfilled for a bounded MSDL ND containing at least one MSTR NT s. t. SD ST and see also Remarks 4-2 (3) in Sect. 4. 3) "one. " Note that this local liveness for ND s. t. SD ST is one of useful necessary conditions for liveness condition of general Petri nets N=(S,T,F,Mo) s. t. S SD. However, because this has not been discussed in literature and is not trivial, some new concepts such as T-cornucopias and return paths are introduced into the real deadlock-trap structure s. t. SD ST in N and this is proven by dividing it into two cases: ND s. t. SD ST is live and unbounded under MoD and ND s. t. SD ST is live and bounded under MoD. Usefulness for the results obtained is also discussed.

Many rewriting systems, including those of terms, strings, graphs, and conjunction of atoms, are used throughout computer science and artificial intelligence. While the concepts of "substitutions," "places" in objects and the "replacement" of "subobjects" by other objects seems to be common to all rewriting systems, there does not exist a common foundation for such systems. At the present time, many of the theories are constructed independently, one for each kind of rewritten object. In the conventional approach, abstract rewriting systems are used to discuss common properties of all rewriting systems. However, they are too abstract to capture properties relating to substructures of objects. This paper aims to provide a first step towards a unified formalization of rewriting systems. The major problem in their formulation may be the formalization of the concept of "places". This has been solved here by employment of the concept of contexts rather than by formalization of places. Places determine subobjects from objects, while, conversely, contexts determine objects from subobjects. A class of rewriting systems, called β rewriting systems, is proposed. It is defined on axiomatically formulated base structures, called β structures, which are used to formalize the concepts of "contexts" and "replacement" common to many rewritten objects. The class of β rewriting systems includes very important systems such as semi-Thue systems and Petri Nets. Abstract rewriting systems are also a subclass of β rewriting systems.

Petri net is a graphical and mathematical tool for modelling, analysis, verification, and evaluation of discrete event systems. Liveness is one of the most important problems of Petri net analysis. This is concerned with a capability for firing of transitions and can be interpreted as a problem to decide whether the system under consideration is always able to reach a stationary behavior, or to decide whether the system is free from any redundant elements. An asymmetric choice (AC) net is a superclass of useful subclasses such as EFCs, FCs, SMs, and MGs, where SMs admit no synchronization, MGs admit no conflicts, FCs as well as EFCs admit no confusion, and ACs allow asymmetric confusion but disallow symmetric confusion. It is known that an AC net N is live iff it is place-live, but this is not the "initial-marking-based" condition and place-liveness is in general hard to test. For the initial-marking-based liveness for AC nets, it is only known that an AC net N is live if (but not only if) every deadlock in N contains a marked structural trap.

Petrify is a tool for (1) manipulating concurrent specifications and (2) synthesis and optimization of asynchronous control circuits. Given a Petri Net (PN), a Signal Transition Graph (STG), or a Transition System (TS) it (1) generates another PN or STG which is simpler than the original description and (2) produces an optimized net-list of an asynchronous controller in the target gate library while preserving the specified input-output behavior. An ability of back-annotating to the specification level helps the designer to control the design process. For transforming a specification petrify performs a token flow analysis of the initial PN and produces a transition system (TS). In the initial TS, all transitions with the same label are considered as one event. The TS is then transformed and transitions relabeled to fulfill the conditions required to obtain a safe irredundant PN. For synthesis of an asynchronous circuit petrify performs state assignment by solving the Complete State Coding problem. State assignment is coupled with logic minimization and speed-independent technology mapping to a target library. The final net-list is guaranteed to be speed-independent, i.e., hazard-free under any distribution of gate delays and multiple input changes satisfying the initial specification. The tool has been used for synthesis of PNs and PNs composition, synthesis and re-synthesis of asynchronous controllers and can be also applied in areas related with the analysis of concurrent programs. This paper provides an overview of petrify and the theory behind its main functions.

This paper proposes a synthesis method to obtain speed-independent asynchronous circuits directly from signal transition graph (STG) specifications with single cycle signals which can be non-persistent and have free-choice operations. The resulting circuits are implemented with basic gates and asynchronous latches, and operate correctly under finite but unbounded gate delays and the zero wire delay assumptions. The proposed method introduces 5 types of lock relations to implement a non-persistent STG. A non-persistent STG can be implemented if every non-persistent signal to a signal t is super-locked with t. The resulting circuits are optimized by extracting of literals, mapping onto asymmetric C-elements, etc. Experimental results show that the proposed synthesis method outperforms the existing synthesis systems such as SYN and SIS.

A formal system-level synthesis model for the concurrent object-oriented design of parallel computer systems, called Multi-token Object-oriented Bi-directional net (MOBnet), is proposed. The MOBnet model extends the standard Petri net by defining (1) multiple tokens to represent different kinds of synthesis control information, (2) object-oriented nodes (places) to denote the system parts under synthesis, and (3) bi-directional arcs to model the design completion check and synthesis rollback operations. In this paper, we first show that MOBnet can serve as a pre-fabrication design methodology analysis tool in ways such as class hierarchy construction, design specification comparison, reachability analysis, and concurrent process management and analysis. We then formally prove MOBnet to be a valid model for concurrent synthesis and give experimental application examples to verify. Finally, solution schemes for the design completion check and synthesis rollback problems are formally validated by analyzing the dynamic behavior of MOBnet, and experimentally illustrated through examples.

This paper deals with the synthesis of Petri nets. Partial languages adequately represent the concurrent behaviors of Petri nets. We first propose a construction problem for Petri nets, in which the objective is to synthesize a Petri net to exhibit the desired behavior specified as a partial language. We next discuss the solvability of this problem and last present the cutline of a solution technique.

A siphon (or alternatively a structutal deadlock) of a Petri net is defined as a set S of places such that existence of any edge from a transition t to a place of S implies that there is an edge from some place of S to t. A minimal siphon is a siphon such that any proper subset is not a siphon. The results of the paper are as follows. (1) The problem of deciding whether or not a given Petri net has a minimum siphon (i.e., a minimum-cardinality minimal siphon) is NP-complete. (2) A polynomial-time algorithm to find, if any, a minimal siphon or even a maximal calss of mutually disjoint minimal siphons of a general Petri net is proposed.

A minimal siphon (or alternatively a structural deadlock) of a Petri net is defined as a minimal set S of places such that existence of any edge from a transition t to a place of S implies that there is an edge from some place of S to t. The subject of the paper is to find a minimal siphon containing a given set of specified places of a general Petri net.

Petri nets are widely recognized as a powerful model for discrete event systems. Petri nets have both graphical and mathematical features. Graphical feature provides an environment to design and to comprehend discrete event systems. Mathematical feature provides an analysis power for verifying several properties of such systems. Several analysis techniques have been proposed so far, such as a reachability (coverability) graph method, a matrix equation approach, reduction or decomposition techniques, a symbolic model method and an unfolding method. The unfolding method was introduced to avoid generating the reachability graph. Unfoldings are often used in the verification of asynchronous circuits. This paper focuses on an analysis of finite state systems, i.e., bounded nets, and discuss a reachability problem and a upper bound problem. Relations between these problems and an unfolding have been clarified to provide a novel method to resolve these problems.

In this paper we present an efficient method to solve reachability problems for Petri nets based on genetic algorithms and a kind of random search which is called postpone search. Genetic algorithm is one of algorithms developed for solving several problems of optimization. We apply GAs and postpone search to approximately solving reachability problems. This approach can not determine exact solutions, however, from applicability points of view, does not directly face state space explosion problems and can extend class of Petri nets to deal with very large state space in reasonable time. First we describe how to represent reachability problems on each of GAs and postpone search. We suppose the existence of a nonnegative parickh vector which satisfies the necessary reachability condition. Possible firing sequences of transitions induced by the parickh vector is encoded on GAs. We also define fitness function to solve reachability problems. Reachability problems can be interpreted as an optimization ones on GAs. Next we introduce random reachability problems which are capable of handling state space and the number of firing sequences which enable to reach a target marking from an initial marking. State space and the number of firing sequences are considered as factors which effect on the hardness of reachability problems to solve with stochastic methods. Furthermore, by using those random reachability problems and well known dining philosophers problems as benchmark problems, we compare GAs' performance with the performance of postpone search. Finally we present empirical results that GAa is more useful method than postpone search for solving more harder reachability problems from the both points of view; reliability and efficiency.

This paper concerns a Petri-net-based model for describing reactive and concurrent systems. Although many high-level Petri nets have been proposed, they are insufficiently practical to describe reactive and concurrent systems in the detail modeling, design and implementation phases. They are mainly intended to describe concurrent systems in the rough modeling phase and lack in several important features (e.g., concurrent tasks, task communication/synchronization, I/O interface, task scheduling) which the most actual implementations of reactive and concurrent systems have. Therefore it is impossible to simulate and analyze the systems accurately without explicitly modeling these features. On the other hand, programming languages based on Petri nets are deeply dependent on their execution environments and not sophisticated as modeling and specification languages. This paper proposes MENDEL net which is a high-level Petri net extended by incorporating concurrent tasks, task communication/synchronization, I/O interface, and task scheduling in a sophisticated manner. MENDEL nets are a wide-spectrum modeling language, that is, they are suitable for not only modeling but also designing and implementing reactive and concurrent systems.

We develop a new class of stochastic Petri net: non-regenerative stochastic Petri net (NRSPN), which allows the firing time of its transitions with arbitrary distributions, and can automatically generate a bounded reachability graph that is equivalent to a generalization of the Markov renewal process in which some of the states may not constitute regeneration points. Thus, it can model and analyze behavior of a system whose states include some non-regeneration points. We show how to model a system by the NRSPN, and how to obtain numerical solutions for the NRSPN model. The probabilistic behavior of the modeled system can be clarified with the reliability measures such as the steady-state probability, the expected numbers of visits to each state per unit time, availability, unavailability and mean time between system failure. Finally, to demonstrate the modeling ability and analysis power of the NRSPN model, we present an example for a fault-tolerant system using the NRSPN and give numerical results for specific distributions.

Petri net is a graphical and mathematical modeling tool for discrete event systems. This paper treats analysis problems for Petri nets under the earliest firing rule. Under this firing rule, transitions must fire as soon as they are enabled. Marked Petri nets under the earliest firing rule are called earliest firing systems, for short. First, some relations in analysis problems between the earliest and the normal firing systems are discussed. These problems include deadlock freedom, boundedness, persistency and liveness. Then, relations among three types of reachability are considered from the viewpoint of the earliest firing rule. Since earliest firing systems can simulate register machines, they have equivalent modeling powers to Turing machines. It suggests, however, that most of the analysis problems of earliest firing systems with general net structures are undecidable. In this paper, net structures are restricted to a subclass called dissynchronous choice (DC) nets. It is shown that the reachability problem from an initial marking to dead markings (markings where no transition can fire) in earliest firing DC systems is equivalent to the usual reachability problem of the same systems under the normal firing rule. Then, the result is applied to reachability problems of controlled DC systems in which some transitions in the net have external control input places. It is shown that for systems where every transition in the net has an external control input place, one type of reachability problem is decidable. Lastly, the liveness problem of earliest firing DC systems is considered and it is shown that this problem is equivalent to that of the underlying DC system under the normal firing rule. It is also shown that this liveness problem is decidable.

In this paper, we show that by suitably selecting a notation to construct synchronization requirement specifications (SRS) for multimedia presentation we can express the timing characteristics at an abstract level, verify the specification, and obtain a hardware implementation through a sequence of transformations of the specification. First, we introduce the notion of a well-formed SRS and its hardware model. Second, we model an SRS as a timed Petri net and interpret the transitions of the net as hardware signals. To obtain logic functions from the SRS, we simplify the net and obtain a signal transition graph satisfying the unique state coding property. Finally, we show how to obtain a logic-level design of synchronizers.

Petri nets are useful in modeling and analyzing various types of discrete-event systems such as parallel processing systems, distributed systems, and sequential control systems, because Petri nets can easily be used to represent such properties of these systems as concurrency, nondecidability, and causality. Various behavioral analytic problems on Petri nets are reduced to reachability and liveness on them. It is also known that the decidability of liveness is equivalent to that of reachability which is solvable. However, useful necessary and sufficient structural liveness conditions have been given only for extended free-choice (EFC) nets and their subclasses. Moreover recently, a necessary and sufficient structural liveness condition for a useful subclass NKT=(SKT, TKT, FKT, MoKT) (i.e., a Petri net in which each minimal structural deadlock (MSDL) contains at least one real or virtual kindling trap, each locally structural-live MSDL ND=(SD, TD, FD, MoD) is never globally dead even if all key transitions for local liveness of each MSDL are controlled by the net of SKTSD s.t. SKTSD, and there exists no singular MSDL of type (α)) has also been given. In this paper, in order to give one of the bases for a necessary and sufficient "structural" or "initial-marking-based" liveness condition for a general Petri net N, we will, first, directly present a necessary and sufficient local liveness condition for each MSDL with a real deadlock-trap structure in a subclass Ñ (N) using the net structure and initial token distribution and extending basic concepts used in NKT, where Ñ is a general Petri net without live behavioral traps, local liveness means a useful necessary condition for the above final goal, and real deadlock-trap structure means that each MSDL in Ñ contains at least one minimal structural trap. Secondly, a new subclass is shown in which, if the above locally structural liveness condition for each MSDL holds, then the whole-net liveness is also guaranteed. It is also argued that the obtained results are applicable to describing new live behavioral traps and deriving a necessary and sufficient structural liveness condition, which is the final goal in this work, for a general Petri net N.

Up to now, the only useful and well-known structural or initial-marking-based necessary and sufficient liveness conditions of Petri nets have only been those of an extended free-choice (EFC) net and its subclasses such as a free-choice (FC) net, a forward conflict free (FCF) net, a marked graph (MG), and a state machine (SM). All the above subclasses are activated only by deadlock-trap properties (i.e., real d-t properties in this paper), which mean that every minimal structural deadlock (MSDL ND=(SD, TD, FD, MoD)) in a net contains at least one live minimal structural trap (MSTR NT=(ST, TT, FT, MoT)) which is initially marked. However, the necessary and sufficient liveness conditions for EFCF, EBCF, EMGEFCFEBCF, AC (EFCFC), and the net with kindling traps NKT have recently been determined, in which each MSDL without real d-t properties was also activated by a new type of trap of trap, i.e., behavioral traps (BTRs), which are defined by introducing a virtual MSTR, a virtual maximal structural trap (virtual STR), a virtual MSDL, and a virtual maximal structural deadlock (virtual SDL) into a target MSDL. In this paper, a structural or initial-marking-based necessary and sufficient condition for local liveness (i.e., virtual deadlock-trap properties) of each MSDL ND s.t. SDST, SDST, SDST (but ND s.t. SDST is dead owing to real deadlock-trap properties) in a general Petri net N is presented by extending that in NKT. Specifically, live minimal behavioral traps (MBTRs) as well as live maximal behavioral traps (BTRs), i.e., virtual deadlock-trap properties, in a general Petri net N are characterized using the real d-t properties of each MSDL ND s.t. SDST for a general Petri net N, which were also obtained by extending the concept of return paths in NKT in connection with an MSDL which contains at least one MSTR and by using the concepts of T-cornucopias and absolute T-cornucopias in a subclass Ñ of N. In other words, BTRs are defined by introducing a virtual MSTR, a virtual STR, a virtual MSDL, and a virtual SDL into a target MSDL without real d-t properties. Additionally, a structural or initial-marking-based necessary and sufficient condition for liveness of a new subclass Nn of a general Petri net N (i.e., a general Petri net without time) is derived, and the usefulness of the obtained results is also discussed.

If a general Petri net N = (S, T, F, Mo) is transition-live under Mo, it is evident that each maximal structural deadlock SDL(D) in N as well as each minimal structural deadlock MSDL (ND) in each D is also transition-live under Mo. However, since the converse of the latter of the above is not always true, it is important to obtain the conditions for this converse to be true if we want to have a useful necessary and sufficient "initial-marking-based" or "structural" liveness condition for N. Up to now, usefull and well-known structural or initial-marking-based necessary and sufficient liveness conditions of Petri nets have only been those of an asymmetric choice (AC) net and its subclasses such as an EFC net, an FC net, an FCF net, MG, and SM. However, all the above subclasses are activated only by real or virtual deadlock-trap properties which are local liveness for each minimal deadlocks; in other words, the above topics of this paper are unconditionally satisfied in those subclasses because of their special structure of nets. In this paper, a necessary and sufficient structural liveness condition for a general Petri net N with globally structural live minimal structural deadlocks is presented as follows: The next () or () is satisfied. () N has no SDL D. () If N has at least one SDL D, () or () is satisfied under the condition that each MSDL ND in N is transition-live under Mo. () N has no singular MSDL (α) (i.e., (α-) and (α-)). () If N has at least one singular MSDL (α-)((α-), resp.), every semi-MDSL ()((), resp.) NDS = (SDS, TDS, FDS, MoDS with respect to each singular MSDL (α-)((α-), resp.), is transition-live under the MoDS under the condition of "the condition (**)", where the locally structural liveness for this NDS means (1) or (2)((3), resp.) of Lemma 4-4 and "the condition (**)" is defined in Lemma 4-7 of this paper. The relationship between the above results and the liveness problem for N is also shown.